Inference at * 1 1 1 1 1 
Iof proof for Lemma bij imp exists inv:



1. A : Type
2. B : Type
3. f : AB
4. a1, a2:A. (f(a1) = f(a2))  (a1 = a2)
5. g : BA
6. b:B. f(g(b)) = b
  InvFuns(A;B;f;g) 

latex

 by D 0 

latex

 1: 

 1:   (g o f) = Id{A}
 2: 

 2:   (f o g) = Id{B}
 .

Definitions	P & Q, InvFuns(A;B;f;g)
Lemmas	inv funs wf